1 /-
2 Copyright (c) 2019 Scott Morrison. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Scott Morrison
5 -/
6 import topology.sheaves.presheaf
src └───────────────────────┘
7
8 /-!
9 # Presheafed spaces
10
11 Introduces the category of topological spaces equipped with a presheaf (taking values in an
12 arbitrary target category `C`.)
13
14 We further describe how to apply functors and natural transformations to the values of the
15 presheaves.
16 -/
17
18 universes v u
19
20 open category_theory
21 open Top
22 open topological_space
23 open opposite
24 open category_theory.category category_theory.functor
25
26 variables (C : Type u) [𝒞 : category.{v} C]
id └──┘ └──────┘
src └──────┘
typ └──┘ └──────┘
doc └──────┘
27 include 𝒞
28
29 local attribute [tidy] tactic.op_induction'
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──┘
30
31 namespace algebraic_geometry
32
33 /-- A `PresheafedSpace C` is a topological space equipped with a presheaf of `C`s. -/
34 structure PresheafedSpace :=
35 (to_Top : Top.{v})
id └─┘
src └─┘
typ └─┘
doc └─┘
36 (𝒪 : to_Top.presheaf C)
id └────┘└───────┘ ┴
src └───────┘
typ └────┘└───────┘ ┴
37
38 variables {C}
39
40 namespace PresheafedSpace
41
42 instance coe_to_Top : has_coe (PresheafedSpace.{v} C) Top :=
id └─────┘ └─────────────┘ ┴ └─┘
src └─────┘ └─────────────┘ └─┘
typ └─────┘ └─────────────┘ ┴ └─┘
doc └─────────────┘ └─┘
43 { coe := λ X, X.to_Top }
id ┴ ┴└─────┘
src └─────┘
typ ┴ ┴└─────┘
44
45 @[simp] lemma as_coe (X : PresheafedSpace.{v} C) : X.to_Top = (X : Top.{v}) := rfl
id └─────────────┘ ┴ ┴└─────┘ ┴ ┴ └─┘ └─┘
src └─────────────┘ └─────┘ ┴ └─┘ └─┘
typ └─────────────┘ ┴ ┴└─────┘ ┴ ┴ └─┘ └─┘
doc └──┘ └─────────────┘ └─┘
46 @[simp] lemma mk_coe (to_Top) (𝒪) : (({ to_Top := to_Top, 𝒪 := 𝒪 } :
id └────┘ ┴
typ └────┘ ┴
doc └──┘
47 PresheafedSpace.{v} C) : Top.{v}) = to_Top := rfl
id └─────────────┘ ┴ └─┘ ┴ └────┘ └─┘
src └─────────────┘ └─┘ ┴ └─┘
typ └─────────────┘ ┴ └─┘ ┴ └────┘ └─┘
doc └─────────────┘ └─┘
48
49 instance (X : PresheafedSpace.{v} C) : topological_space X := X.to_Top.str
id └─────────────┘ ┴ └───────────────┘ ┴ ┴└─────┘└──┘
src └─────────────┘ └───────────────┘ └─────┘└──┘
typ └─────────────┘ ┴ └───────────────┘ ┴ ┴└─────┘└──┘
doc └─────────────┘ └───────────────┘
50
51 /-- A morphism between presheafed spaces `X` and `Y` consists of a continuous map
52 `f` between the underlying topological spaces, and a (notice contravariant!) map
53 from the presheaf on `Y` to the pushforward of the presheaf on `X` via `f`. -/
54 structure hom (X Y : PresheafedSpace.{v} C) :=
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └─────────────┘
55 (f : (X : Top.{v}) ⟶ (Y : Top.{v}))
id ┴ └─┘ ┴ ┴ └─┘
src └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ └─┘
doc └─┘ └─┘
56 (c : Y.𝒪 ⟶ f _* X.𝒪)
id ┴└┘ ┴ ┴ └┘ ┴└┘
src └┘ ┴ └┘ └┘
typ ┴└┘ ┴ ┴ └┘ ┴└┘
57
58 @[ext] lemma ext {X Y : PresheafedSpace.{v} C} (α β : hom X Y)
id └─────────────┘ ┴ └─┘ ┴ ┴
src └─────────────┘ └─┘
typ └─────────────┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────┘ └─┘
59 (w : α.f = β.f) (h : α.c ≫ (whisker_right (nat_trans.op (opens.map_iso _ _ w).inv) X.𝒪) = β.c) :
id ┴└┘ ┴ ┴└┘ ┴└┘ ┴ └───────────┘ └──────────┘ └───────────┘ ┴ └─┘ ┴└┘ ┴ ┴└┘
src └┘ ┴ └┘ └┘ ┴ └───────────┘ └──────────┘ └───────────┘ └─┘ └┘ ┴ └┘
typ ┴└┘ ┴ ┴└┘ ┴└┘ ┴ └───────────┘ └──────────┘ └───────────┘ ┴ └─┘ ┴└┘ ┴ ┴└┘
60 α = β :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
61 begin
st └─────
62 cases α, cases β,
id ┴ ┴
src └────┘ └────┘
typ └────┘┴ └────┘┴
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ────────┘└───────┘└─
63 dsimp [presheaf.pushforward] at *,
id └──────────────────┘
src └─────┘└──────────────────┘└────┘
typ └─────┘└──────────────────┘└────┘
doc └─────┘ └────┘
txt └─────┘ └────┘
par └─────┘ └────┘
pid ┴┴ ┴┴└──┘
st ──────────────────────────────────┘└─
64 tidy, -- TODO including `injections` would make tidy work earlier.
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└──────────────────────────────────────────────────────────────
65 end
st ──┘
66 .
67
68 def id (X : PresheafedSpace.{v} C) : hom X X :=
id └─────────────┘ ┴ └─┘ ┴ ┴
src └─────────────┘ └─┘
typ └─────────────┘ ┴ └─┘ ┴ ┴
doc └─────────────┘ └─┘
69 { f := 𝟙 (X : Top.{v}),
id ┴ ┴ └─┘
src ┴ └─┘
typ ┴ ┴ └─┘
doc └─┘
70 c := ((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.to_Top)).hom) _) }
id └─────────────────┘ └─┘ ┴ └───────────┘ └──────────┘ └──────────┘ ┴└─────┘ └─┘
src └─────────────────┘ └─┘ ┴ └───────────┘ └──────────┘ └──────────┘ └─────┘ └─┘
typ └─────────────────┘ └─┘ ┴ └───────────┘ └──────────┘ └──────────┘ ┴└─────┘ └─┘
71
72 def comp (X Y Z : PresheafedSpace.{v} C) (α : hom X Y) (β : hom Y Z) : hom X Z :=
id └─────────────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─────────────┘ └─┘ └─┘ └─┘
typ └─────────────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └─────────────┘ └─┘ └─┘ └─┘
73 { f := α.f ≫ β.f,
id ┴└┘ ┴ ┴└┘
src └┘ ┴ └┘
typ ┴└┘ ┴ ┴└┘
74 c := β.c ≫ (whisker_left (opens.map β.f).op α.c) }
id ┴└┘ ┴ └──────────┘ └───────┘ ┴└┘ └┘ ┴└┘
src └┘ ┴ └──────────┘ └───────┘ └┘ └┘ └┘
typ ┴└┘ ┴ └──────────┘ └───────┘ ┴└┘ └┘ ┴└┘
doc └───────┘
75
76 variables (C)
77
78 section
79 local attribute [simp] id comp presheaf.pushforward
id └┘ └──┘ └──────────────────┘
src └┘ └──┘ └──────────────────┘
typ └┘ └──┘ └──────────────────┘
doc └──┘
80
81 /- The proofs below can be done by `tidy`, but it is too slow,
82 and we don't have a tactic caching mechanism. -/
83 /-- The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map
84 from the presheaf on the target to the pushforward of the presheaf on the source. -/
85 instance category_of_PresheafedSpaces : category (PresheafedSpace.{v} C) :=
id └──────┘ └─────────────┘ ┴
src └──────┘ └─────────────┘
typ └──────┘ └─────────────┘ ┴
doc └──────┘ └─────────────┘
86 { hom := hom,
id └─┘
src └─┘
typ └─┘
doc └─┘
87 id := id,
id └┘
src └┘
typ └┘
88 comp := comp,
id └──┘
src └──┘
typ └──┘
89 id_comp' := λ X Y f,
id ┴ ┴ ┴
typ ┴ ┴ ┴
90 begin
st └─────
91 ext1, swap,
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st ───────┘└────┘└─
92 { dsimp, simp only [id_comp] },
id └─────┘
src └───┘ └─────────┘└─────┘└┘
typ └───┘ └─────────┘└─────┘└┘
doc └───┘ └─────────┘ └┘
txt └───┘ └─────────┘ └┘
par └───┘ └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st ─────┘└───┘└────────────────────┘└┘└
93 { ext U,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────────┘└─
94 op_induction,
src └──────────┘
typ └──────────┘
txt └──────────┘
par └──────────┘
st ─────────────────┘└─
95 cases U,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
96 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
97 simp only [comp_id, map_id] },
id └─────┘ └────┘
src └─────────┘└─────┘└┘└────┘└┘
typ └─────────┘└─────┘└┘└────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ─────────────────────────────────┘└──
98 end,
st ────┘
99 comp_id' := λ X Y f,
id ┴ ┴ ┴
typ ┴ ┴ ┴
100 begin
st └─────
101 ext1, swap,
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st ───────┘└────┘└─
102 { dsimp, simp only [comp_id] },
id └─────┘
src └───┘ └─────────┘└─────┘└┘
typ └───┘ └─────────┘└─────┘└┘
doc └───┘ └─────────┘ └┘
txt └───┘ └─────────┘ └┘
par └───┘ └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st ─────┘└───┘└────────────────────┘└┘└
103 { ext U,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────────┘└─
104 op_induction,
src └──────────┘
typ └──────────┘
txt └──────────┘
par └──────────┘
st ─────────────────┘└─
105 cases U,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
106 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
107 simp only [comp_id, id_comp, map_id] }
id └─────┘ └─────┘ └────┘
src └─────────┘└─────┘└┘└─────┘└┘└────┘└┘
typ └─────────┘└─────┘└┘└─────┘└┘└────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st ──────────────────────────────────────────┘└─
108 end,
st ────┘
109 assoc' := λ W X Y Z f g h,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
110 begin
st └─────
111 simp only [true_and, presheaf.pushforward, id, comp, whisker_left_twice, whisker_left_comp,
id └──────┘ └──────────────────┘ └┘ └──┘ └────────────────┘ └───────────────┘
src └─────────┘└──────┘└┘└──────────────────┘└┘└┘└┘└──┘└┘└────────────────┘└┘└───────────────┘└─
typ └─────────┘└──────┘└┘└──────────────────┘└┘└┘└┘└──┘└┘└────────────────┘└┘└───────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────────────
112 heq_iff_eq, category.assoc],
id └────────┘ └────────────┘
src ──────────────┘└────────┘└┘└────────────┘┴
typ ──────────────┘└────────┘└┘└────────────┘┴
doc ──────────────┘ └┘ ┴
txt ──────────────┘ └┘ ┴
par ──────────────┘ └┘ ┴
pid ──────────────┘ └┘ ┴
st ─────────────────────────────────────────┘└─
113 split; refl
src └───┘ └────
typ └───┘ └────
doc └───┘ └────
txt └───┘ └────
par └───┘ └────
pid └
st ────────────────
114 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
115
116 end
117
118 variables {C}
119
120 instance {X Y : PresheafedSpace.{v} C} : has_coe (X ⟶ Y) (X.to_Top ⟶ Y.to_Top) :=
id └─────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴└─────┘ ┴ ┴└─────┘
src └─────────────┘ └─────┘ ┴ └─────┘ ┴ └─────┘
typ └─────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴└─────┘ ┴ ┴└─────┘
doc └─────────────┘
121 { coe := λ α, α.f }
id ┴ ┴└┘
src └┘
typ ┴ ┴└┘
122
123 @[simp] lemma hom_mk_coe {X Y : PresheafedSpace.{v} C} (f) (c) :
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └──┘ └─────────────┘
124 (({ f := f, c := c } : X ⟶ Y) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘
src ┴ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘
doc └─┘ └─┘
125 @[simp] lemma f_as_coe {X Y : PresheafedSpace.{v} C} (α : X ⟶ Y) :
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └──┘ └─────────────┘
126 α.f = (α : (X : Top.{v}) ⟶ (Y : Top.{v})) := rfl
id ┴└┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─┘
src └┘ ┴ └─┘ ┴ └─┘ └─┘
typ ┴└┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └─┘
doc └─┘ └─┘
127 @[simp] lemma id_coe (X : PresheafedSpace.{v} C) :
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └──┘ └─────────────┘
128 (((𝟙 X) : X ⟶ X) : (X : Top.{v}) ⟶ X) = 𝟙 (X : Top.{v}) := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘
src ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘
doc └─┘ └─┘
129 @[simp] lemma comp_coe {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────────┘
130 ((α ≫ β : X ⟶ Z) : (X : Top.{v}) ⟶ Z) = (α : (X : Top.{v}) ⟶ Y) ≫ (β : Y ⟶ Z) := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └─┘ └─┘
131
132 lemma id_c (X : PresheafedSpace.{v} C) :
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └─────────────┘
133 ((𝟙 X) : X ⟶ X).c =
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
134 (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.to_Top)).hom) _)) := rfl
id └─────────────────┘ └─┘ ┴ └───────────┘ └──────────┘ └──────────┘ ┴└─────┘ └─┘ └─┘
src └─────────────────┘ └─┘ ┴ └───────────┘ └──────────┘ └──────────┘ └─────┘ └─┘ └─┘
typ └─────────────────┘ └─┘ ┴ └───────────┘ └──────────┘ └──────────┘ ┴└─────┘ └─┘ └─┘
135
136 -- Implementation note: this harmless looking lemma causes deterministic timeouts,
137 -- but happily we can survive without it.
138 -- lemma comp_c {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
139 -- (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) := rfl
140
141 @[simp] lemma id_c_app (X : PresheafedSpace.{v} C) (U) :
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └──┘ └─────────────┘
142 ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { op_induction U, cases U, refl }) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └───────┘ ┴
src ┴ ┴ ┴ └─┘ ┴ └───────┘ └────────────┘ └────┘ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └───────┘ └────────────┘ └────┘┴ └───┘
doc └────┘ └───┘
txt └────────────┘ └────┘ └───┘
par └────────────┘ └────┘ └───┘
pid └┘ ┴ ┴
st └───────────────┘└───────┘└─────┘└┘
143 by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
id ┴ └──┘
src └────────────┘ └────┘ └─────────┘└──┘┴ └───┘ └──┘
typ └────────────┘ └────┘┴ └─────────┘└──┘┴ └───┘ └──┘
doc └────┘ └─────────┘ ┴ └───┘ └──┘
txt └────────────┘ └────┘ └─────────┘ ┴ └───┘ └──┘
par └────────────┘ └────┘ └─────────┘ ┴ └───┘ └──┘
pid └┘ ┴ ┴└──┘└┘ ┴
st └───────────────┘└───────┘└────────────────┘└─────┘└────┘└──┘
144
145 @[simp] lemma comp_c_app {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────────┘
146 (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.f)).obj (unop U))) := rfl
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└┘ └─┘ ┴ ┴ ┴└┘ └─┘ └┘ └───────┘ ┴└┘ └─┘ └──┘ ┴ └─┘
src ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └┘ └───────┘ └┘ └─┘ └──┘ └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└┘ └─┘ ┴ ┴ ┴└┘ └─┘ └┘ └───────┘ ┴└┘ └─┘ └──┘ ┴ └─┘
doc └───────┘
147
148 /-- The forgetful functor from `PresheafedSpace` to `Top`. -/
149 def forget : PresheafedSpace.{v} C ⥤ Top :=
id └─────────────┘ ┴ ┴ └─┘
src └─────────────┘ ┴ └─┘
typ └─────────────┘ ┴ ┴ └─┘
doc └─────────────┘ ┴ └─┘
150 { obj := λ X, (X : Top.{v}),
id ┴ ┴ ┴ └─┘
src ┴ └─┘
typ ┴ ┴ ┴ └─┘
doc ┴ └─┘
151 map := λ X Y f, f }
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
152
153 end PresheafedSpace
154
155 end algebraic_geometry
156
157 open algebraic_geometry algebraic_geometry.PresheafedSpace
158
159 variables {C}
160
161 namespace category_theory
162
163 variables {D : Type u} [𝒟 : category.{v} D]
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
164 include 𝒟
165
166 local attribute [simp] presheaf.pushforward
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──┘
167
168 namespace functor
169
170 /-- We can apply a functor `F : C ⥤ D` to the values of the presheaf in any `PresheafedSpace C`,
171 giving a functor `PresheafedSpace C ⥤ PresheafedSpace D` -/
172 /- The proofs below can be done by `tidy`, but it is too slow,
173 and we don't have a tactic caching mechanism. -/
174 def map_presheaf (F : C ⥤ D) : PresheafedSpace.{v} C ⥤ PresheafedSpace.{v} D :=
id ┴ ┴ ┴ └─────────────┘ ┴ ┴ └─────────────┘ ┴
src ┴ └─────────────┘ ┴ └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └─────────────┘ ┴
doc ┴ └─────────────┘ ┴ └─────────────┘
175 { obj := λ X, { to_Top := X.to_Top, 𝒪 := X.𝒪 ⋙ F },
id ┴ ┴└─────┘ ┴└┘ ┴ ┴
src └─────┘ └┘ ┴
typ ┴ ┴└─────┘ ┴└┘ ┴ ┴
doc ┴
176 map := λ X Y f, { f := f.f, c := whisker_right f.c F },
id ┴ ┴ ┴ ┴└┘ └───────────┘ ┴└┘ ┴
src └┘ └───────────┘ └┘
typ ┴ ┴ ┴ ┴└┘ └───────────┘ ┴└┘ ┴
177 map_id' := λ X,
id ┴
typ ┴
178 begin
st └─────
179 ext1, swap,
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st ───────┘└────┘└─
180 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────┘└───┘└┘└
181 { ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────────┘└─
182 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
183 simp only [presheaf.pushforward, eq_to_hom_map, map_id, comp_id, id_c_app],
id └──────────────────┘ └───────────┘ └────┘ └─────┘ └──────┘
src └─────────┘└──────────────────┘└┘└───────────┘└┘└────┘└┘└─────┘└┘└──────┘┴
typ └─────────┘└──────────────────┘└┘└───────────┘└┘└────┘└┘└─────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────┘└─
184 refl }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└─
185 end,
st ────┘
186 map_comp' := λ X Y Z f g,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
187 begin
st └─────
188 ext1, swap,
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st ───────┘└────┘└─
189 { refl, },
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└──┘└──┘└
190 { ext, dsimp, simp only [comp_id, assoc, map_comp, map_id], },
id └─────┘ └───┘ └──────┘ └────┘
src └─┘ └───┘ └─────────┘└─────┘└┘└───┘└┘└──────┘└┘└────┘┴
typ └─┘ └───┘ └─────────┘└─────┘└┘└───┘└┘└──────┘└┘└────┘┴
doc └─┘ └───┘ └─────────┘ └┘ └┘ └┘ ┴
txt └─┘ └───┘ └─────────┘ └┘ └┘ └┘ ┴
par └─┘ └───┘ └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ────────┘└─────┘└────────────────────────────────────────────┘└────
191 end }
st ────┘
192
193 @[simp] lemma map_presheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
id ┴ ┴ ┴ └─────────────┘ ┴
src ┴ └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ ┴
doc └──┘ ┴ └─────────────┘
194 ((F.map_presheaf.obj X) : Top.{v}) = (X : Top.{v}) := rfl
id ┴└───────────┘└──┘ ┴ └─┘ ┴ ┴ └─┘ └─┘
src └───────────┘└──┘ └─┘ ┴ └─┘ └─┘
typ ┴└───────────┘└──┘ ┴ └─┘ ┴ ┴ └─┘ └─┘
doc └───────────┘ └─┘ └─┘
195 @[simp] lemma map_presheaf_obj_𝒪 (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
id ┴ ┴ ┴ └─────────────┘ ┴
src ┴ └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ ┴
doc └──┘ ┴ └─────────────┘
196 (F.map_presheaf.obj X).𝒪 = X.𝒪 ⋙ F := rfl
id ┴└───────────┘└──┘ ┴ ┴ ┴ ┴└┘ ┴ ┴ └─┘
src └───────────┘└──┘ ┴ ┴ └┘ ┴ └─┘
typ ┴└───────────┘└──┘ ┴ ┴ ┴ ┴└┘ ┴ ┴ └─┘
doc └───────────┘ ┴
197 @[simp] lemma map_presheaf_map_f (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
id ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src ┴ └─────────────┘ ┴
typ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └──┘ ┴ └─────────────┘
198 ((F.map_presheaf.map f) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
id ┴└───────────┘└──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘
src └───────────┘└──┘ └─┘ ┴ └─┘ ┴ └─┘
typ ┴└───────────┘└──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘
doc └───────────┘ └─┘ └─┘
199 @[simp] lemma map_presheaf_map_c (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
id ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src ┴ └─────────────┘ ┴
typ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └──┘ ┴ └─────────────┘
200 (F.map_presheaf.map f).c = whisker_right f.c F := rfl
id ┴└───────────┘└──┘ ┴ ┴ ┴ └───────────┘ ┴└┘ ┴ └─┘
src └───────────┘└──┘ ┴ ┴ └───────────┘ └┘ └─┘
typ ┴└───────────┘└──┘ ┴ ┴ ┴ └───────────┘ ┴└┘ ┴ └─┘
doc └───────────┘
201
202 end functor
203
204 namespace nat_trans
205
206 /- The proofs below can be done by `tidy`, but it is too slow,
207 and we don't have a tactic caching mechanism. -/
208 def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_presheaf :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘ ┴ ┴└───────────┘
src ┴ ┴ └───────────┘ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘ ┴ ┴└───────────┘
doc ┴ └───────────┘ └───────────┘
209 { app := λ X,
id ┴
typ ┴
210 { f := 𝟙 _,
id ┴
src ┴
typ ┴
211 c := whisker_left X.𝒪 α ≫ ((functor.left_unitor _).inv) ≫
id └──────────┘ ┴└┘ ┴ ┴ └─────────────────┘ └─┘ ┴
src └──────────┘ └┘ ┴ └─────────────────┘ └─┘ ┴
typ └──────────┘ ┴└┘ ┴ ┴ └─────────────────┘ └─┘ ┴
212 (whisker_right (nat_trans.op (opens.map_id X.to_Top).hom) _) },
id └───────────┘ └──────────┘ └──────────┘ ┴└─────┘ └─┘
src └───────────┘ └──────────┘ └──────────┘ └─────┘ └─┘
typ └───────────┘ └──────────┘ └──────────┘ ┴└─────┘ └─┘
213 naturality' := λ X Y f,
id ┴ ┴ ┴
typ ┴ ┴ ┴
214 begin
st └─────
215 ext1, swap,
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st ───────┘└────┘└─
216 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────┘└───┘└┘└
217 { ext U,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────────┘└─
218 op_induction,
src └──────────┘
typ └──────────┘
txt └──────────┘
par └──────────┘
st ─────────────────┘└─
219 cases U,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
220 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
221 simp only [comp_id, assoc, map_id, nat_trans.naturality] }
id └─────┘ └───┘ └────┘ └──────────────────┘
src └─────────┘└─────┘└┘└───┘└┘└────┘└┘└──────────────────┘└┘
typ └─────────┘└─────┘└┘└───┘└┘└────┘└┘└──────────────────┘└┘
doc └─────────┘ └┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴
st ──────────────────────────────────────────────────────────────┘└─
222 end }
st ────┘
223
224 -- TODO Assemble the last two constructions into a functor
225 -- `(C ⥤ D) ⥤ (PresheafedSpace C ⥤ PresheafedSpace D)`
226 end nat_trans
227
228 end category_theory